Nuprl Lemma : comb_for_itop_wf
13,42
postcript
pdf
(
A
,
op
,
id
,
p
,
q
,
E
,
z
.
(
op
,
id
)
p
i
<
q
.
E
(
i
))
A
:Type
(
A
A
A
)
A
(
p
,
q
:
({
p
..
q
}
A
)
(
True)
A
)
latex
Up
groups
1
Definitions
t
T
,
,
x
:
A
.
B
(
x
)
,
T
Lemmas
int
seg
wf
,
true
wf
,
squash
wf
,
itop
wf
origin
A,op,id,p,q,E,z. 
(op,id) p 
i < q. E(i))
A:Type
(AAA)A(p,q:
({p..q
}A)(
True)A) A,op,id,p,q,E,z. (op,id) p i < q. E(i))
A:Type(AAA)A(p,q:({p..q}A)(True)A) T
x:A. B(x)T